n:. finite(n) 

latex

Definitions	AB, finite(T), Surj(A; B; f), x. t(x), Dec(P), P  Q, Prop, x:A. B(x), t  T, , i  j < k, P & Q, A, False, P  Q, Inj(A; B; f), x:A. B(x), {i..j}, T, True, if b t else f fi, i=j, Unit, P  Q, , b, b
Lemmas	assert wf, not wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, decidable int equal, le wf, injection le, decidable equal int seg, decidable ex int seg, nat wf, int seg wf, inject wf